Inference at * 
Iof proof for Lemma p-compose wf:


  A, B, C:Type, g:(A(B + Top)), f:(B(C + Top)). f o g    A(C + Top) 

latex

 by ((Auto) 
CollapseTHEN (((Unfold `p-compose` ( 0)) 
CollapseTHEN ((((if (((first_nat 2:n
C)) = 0) then (Repeat (MaAutoStep)) else (RepeatFor (first_nat 2:n) (MaAutoStep)))) 

C)CollapseTHEN ((Try ((Complete (Auto)))))))))) 

latex

C1: 

C1: 1. A : Type
C1: 2. B : Type
C1: 3. C : Type
C1: 4. g : A(B + Top)
C1: 5. B(C + Top)
C1: 6. x : A
C1: 7. (can-apply(g;x))
C1:   g(x)  (C + Top)
C.

Definitions	f o g  , x:A.B(x), Void, if b then t else f fi , suptype(S; T), x.A(x), Unit, , tt, p q, p  q, p  q, [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, P  Q, P & Q, x:A  B(x), b, , can-apply(f;x), ff, , b, do-apply(f;x), P  Q, f(a), Top, left + right, s = t, A, Type, S  T, x:A. B(x), t  T, x:AB(x)
Lemmas	ifthenelse wf, can-apply wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, do-apply wf, top wf, member wf